Step of Proof: fast-fib |
11,40 |
|
Inference at * 1 2 1
Iof proof for Lemma fast-fib:
1. n :
2. 0 < n
3.
a, b:
.
3. {m:
|
3. {
k:
.
3. {(a = fib(k)) 
((k
0) 
(b = 0)) 
((0 < k) 
(b = fib(k - 1))) 
(m = fib((n - 1)+k))}
4. a :
5. b :
6.
b1:
.
6. {m:
|
6. {
k:
.
6. {(a+b = fib(k))
6. {
((k
0) 
(b1 = 0))
6. {
((0 < k) 
(b1 = fib(k - 1)))
6. {
(m = fib((n - 1)+k))}
{m:
|
{
k:
.
{(a = fib(k)) 
((k
0) 
(b = 0)) 
((0 < k) 
(b = fib(k - 1))) 
(m = fib(n+k))}
by InstHyp [a] (-1)
1: .....wf..... NILNIL
1:
a
2:
2: 7. {m:
|
2: 7. {
k:
.
2: 7. {(a+b = fib(k))
2: 7. {
((k
0) 
(a = 0))
2: 7. {
((0 < k) 
(a = fib(k - 1)))
2: 7. {
(m = fib((n - 1)+k))}
2:
{m:
|
2:
{
k:
.
2:
{(a = fib(k)) 
((k
0) 
(b = 0)) 
((0 < k) 
(b = fib(k - 1))) 
(m = fib(n+k))}
.